(declare-fun |main::i@3| () Int)
(declare-fun |main::i@4| () Int)
(declare-fun __POLICY_CHOICE_0 () Int)
(declare-fun |main::i@2| () Int)
(declare-fun __POLICY_CHOICE_2 () Int)
(declare-fun __POLICY_CHOICE_1 () Int)
(declare-fun |main::__CPAchecker_TMP_0@3| () Int)
(declare-fun __VERIFIER_nondet_bool@2 () Int)
(assert (let ((a!1 (or (and (not (<= |main::__CPAchecker_TMP_0@3| 0)) (= __POLICY_CHOICE_1 0)) (and (not (>= |main::__CPAchecker_TMP_0@3| 0)) (= __POLICY_CHOICE_1 1))))(a!2 (or (and (not (<= |main::i@2| 4)) (= __POLICY_CHOICE_2 0)) (and (not (>= |main::i@2| 4)) (= __POLICY_CHOICE_2 1))))) (and (or (and (distinct |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2) a!1 (= |main::i@2| 4) (= |main::i@3| 0) (= __POLICY_CHOICE_0 0)) (or (distinct |main::__CPAchecker_TMP_0@3| __VERIFIER_nondet_bool@2) a!1 a!2 (= |main::i@3| |main::i@2|) (= __POLICY_CHOICE_0 1))) (distinct |main::i@4| (+ 1 |main::i@3|)))))
(assert (let ((a!1 (= (- |main::i@2| 0) (* 2 (div (- |main::i@2| 0) 2))))) (and a!1 (>= |main::i@2| 0) (>= (+ (- 1) |main::i@2|) 0))))
(assert (< |main::i@4| 0))
(check-sat)
